Nuprl Definition : es-first-at
0,22
postcript
pdf
e
is first@
i
s.t.
e
.
P
(
e
) == loc(
e
) =
i
&
P
(
e
) & (
e'
<
e
.
P
(
e'
))
latex
clarification:
es-first-at(
es
;
i
;
e
;
e
.
P
(
e
)) == es-loc(
es
;
e
) =
i
Id &
P
(
e
) & alle-lt(
es
;
e
;
e'
.
P
(
e'
))
latex
Definitions
Id
,
loc(
e
)
,
P
&
Q
,
e
<
e'
.
P
(
e
)
,
A
FDL editor aliases
es-first-at
origin
e'<e. 
P(e'))
Id & P(e) & alle-lt(es;e;e'.P(e')) e'<e. P(e'))
Id & P(e) & alle-lt(es;e;e'.P(e')) e<e'. P(e)A